Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.
Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.
Compute (next_weekday friday).
Definition and2(b1:bool)(b2:bool):=
 match b1 with
 | true => b2
 | false => false
 end.
Notation "x && y" := (and2 x y).
Definition and3(b1:bool)(b2:bool)(b3:bool):=
 if b1&&b2 && b3 then true
 else false.
Compute (and3 true false true).
Module NatPlayground.
Inductive natt:Type:=
  | fucker
  | mother (d:natt).
Definition pred(n:natt):natt:=
  match n with
  | fucker => fucker
  | mother n'=>n'
end.
Fixpoint plus (n:natt)(m:natt):natt:=
  match n with
  | fucker => m
  | mother x => mother(plus x m)
end.
End NatPlayground.
Compute (plus 32768 10).
Fixpoint mul n m :=
  match n with
  |1 => m
  |S x => plus m(mul x m)
  |0=>0
end.
Compute mul 72 10.

Fixpoint temp n m:=
  match n with
  |0=>0
  |1=>m
  |S n'=>plus m(temp n' m)
end.
Definition square n:=
  match n with
  |0=>0
  |1=>1
  |S n'=>plus n(temp n' n)
end.
Compute (square 6).
Definition square_nomulti n:=
  match n with
  |0=>0
  |S n'=>square n'+n'+n'+1
end.
Compute (square_nomulti 6).
Compute (minus 3 2).
Fixpoint gtb n m:=
  match n with
  | O => false
  | S n' =>
    match m with
    | O => true
    | S m' => gtb n' m'
    end
  end.
Compute (gtb 4 2).
Compute (gtb 1 3).
Theorem plus_O_n : forall n : nat, gtb (n+1) 0 = true.
Proof.
  intros n.
  destruct n as [ | n'].
  - reflexivity.
  - reflexivity.
Qed.
Fixpoint f n:=
  match n with
  | 0 => 0
  | 1 => 1
  | S n' =>
    match n' with
      | 0 => 0
      | S n'' => f n' + f n''
    end
  end.
Compute (f 10).
Fixpoint F n:=
  match n with
  | 0 => 0
  | 1 => 1
  | S n' => F n' + F(minus n' 1)
  end.
Compute (F 10).

Theorem add_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)    reflexivity.
  - (* n = S n' *) simpl. rewrite -> IHn'. reflexivity.  Qed.
Theorem plus_n_Sm: forall n m:nat, S(n+m)=n+S(m).
Proof.
  intros n m. induction n as [|n' IHn'].
  - reflexivity.
  - simpl. rewrite->IHn'. reflexivity. Qed.
Theorem add_comm: forall n m:nat, n+m=m+n.
Proof.
  intros n m. induction n as [|n' IHn'].
  - rewrite->add_0_r. reflexivity.
  - simpl. rewrite->IHn'. rewrite->plus_n_Sm. reflexivity. Qed.
Theorem add_assoc: forall n m p:nat, n+(m+p)=(n+m)+p.
Proof.
  intros n m p. induction n as [|n' IHn'].
  - reflexivity.
  - simpl. rewrite->IHn'. reflexivity. Qed.
Fixpoint last (l:natlist)(d:nat):nat :=
  match l with
  | [] => d
  | [a] => a
  | a::l=>last l d
  end.
Definition ht l d:=
  match l with
  | nil=>(d,d)
  | h::t=>(hd 0 l, last l d)
  end.
Compute ht 0.